a, b:, p:( List), F, G:({0..||p||}).
weighted-sum(p;x.(a * (F(x))) + (b * (G(x))))
=
((a * weighted-sum(p;F)) + (b * weighted-sum(p;G)))
  

latex

Definitions	x:A. B(x), t  T, P  Q, A  B, A, False, i  j , , , True, P  Q, P  Q, T, P & Q, {i..j}, ||as||, as @ bs, Y, i  j < k, t  ...$L, S  T, suptype(S; T), Top, Dec(P), P  Q
Lemmas	rationals wf, nat wf, le wf, length wf1, int seg wf, nat properties, ge wf, int inc rationals, qadd wf, squash wf, true wf, qmul zero qrng, mon ident q, qmul wf, length nil, non neg length, length cons, length append, append wf, weighted-sum-split, decidable le, qmul over plus qrng, qmul assoc qrng, qmul ac 1 qrng, mon assoc q, qadd comm q, qadd ac 1 q, weighted-sum wf, length wf nat, top wf